The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

fstsplit(0, x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0, x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0, m) → true
leq(s(n), 0) → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Rewrite Strategy: INNERMOST

(1) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

S is empty.
Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

(5) OrderProof (LOWER BOUND(ID) transformation)

Heuristically decided to analyse the following defined symbols:
fstsplit, sndsplit, leq, length, app, map_f, ring

They will be analysed ascendingly in the following order:
fstsplit < ring
sndsplit < ring
leq < ring
length < ring
app < map_f
app < ring
map_f < ring

(6) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
fstsplit, sndsplit, leq, length, app, map_f, ring

They will be analysed ascendingly in the following order:
fstsplit < ring
sndsplit < ring
leq < ring
length < ring
app < map_f
app < ring
map_f < ring

(7) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

Induction Base:
fstsplit(gen_0':s7_0(0), gen_nil:cons:f6_0(0)) →_R^Ω(1)
nil

Induction Step:
fstsplit(gen_0':s7_0(+(n9_0, 1)), gen_nil:cons:f6_0(+(n9_0, 1))) →_R^Ω(1)
cons(nil, fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0))) →_IH
cons(nil, gen_nil:cons:f6_0(c10_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(8) Complex Obligation (BEST)

(9) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
sndsplit, leq, length, app, map_f, ring

They will be analysed ascendingly in the following order:
sndsplit < ring
leq < ring
length < ring
app < map_f
app < ring
map_f < ring

(10) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)

Induction Base:
sndsplit(gen_0':s7_0(0), gen_nil:cons:f6_0(0)) →_R^Ω(1)
gen_nil:cons:f6_0(0)

Induction Step:
sndsplit(gen_0':s7_0(+(n717_0, 1)), gen_nil:cons:f6_0(+(n717_0, 1))) →_R^Ω(1)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) →_IH
gen_nil:cons:f6_0(0)

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(11) Complex Obligation (BEST)

(12) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
leq, length, app, map_f, ring

They will be analysed ascendingly in the following order:
leq < ring
length < ring
app < map_f
app < ring
map_f < ring

(13) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)

Induction Base:
leq(gen_0':s7_0(0), gen_0':s7_0(0)) →_R^Ω(1)
true

Induction Step:
leq(gen_0':s7_0(+(n1508_0, 1)), gen_0':s7_0(+(n1508_0, 1))) →_R^Ω(1)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) →_IH
true

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(14) Complex Obligation (BEST)

(15) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
length, app, map_f, ring

They will be analysed ascendingly in the following order:
length < ring
app < map_f
app < ring
map_f < ring

(16) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)

Induction Base:
length(gen_nil:cons:f6_0(0)) →_R^Ω(1)
0'

Induction Step:
length(gen_nil:cons:f6_0(+(n1957_0, 1))) →_R^Ω(1)
s(length(gen_nil:cons:f6_0(n1957_0))) →_IH
s(gen_0':s7_0(c1958_0))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(17) Complex Obligation (BEST)

(18) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
app, map_f, ring

They will be analysed ascendingly in the following order:
app < map_f
app < ring
map_f < ring

(19) RewriteLemmaProof (LOWER BOUND(ID) transformation)

Proved the following rewrite lemma:
app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b)) → gen_nil:cons:f6_0(+(n2353_0, b)), rt ∈ Ω(1 + n2353₀)

Induction Base:
app(gen_nil:cons:f6_0(0), gen_nil:cons:f6_0(b)) →_R^Ω(1)
gen_nil:cons:f6_0(b)

Induction Step:
app(gen_nil:cons:f6_0(+(n2353_0, 1)), gen_nil:cons:f6_0(b)) →_R^Ω(1)
cons(nil, app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b))) →_IH
cons(nil, gen_nil:cons:f6_0(+(b, c2354_0)))

We have rt ∈ Ω(n¹) and sz ∈ O(n). Thus, we have irc_R ∈ Ω(n).

(20) Complex Obligation (BEST)

(21) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)
app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b)) → gen_nil:cons:f6_0(+(n2353_0, b)), rt ∈ Ω(1 + n2353₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
map_f, ring

They will be analysed ascendingly in the following order:
map_f < ring

(22) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol map_f.

(23) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)
app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b)) → gen_nil:cons:f6_0(+(n2353_0, b)), rt ∈ Ω(1 + n2353₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

The following defined symbols remain to be analysed:
ring

(24) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

Could not prove a rewrite lemma for the defined symbol ring.

(25) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)
app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b)) → gen_nil:cons:f6_0(+(n2353_0, b)), rt ∈ Ω(1 + n2353₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(26) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(27) BOUNDS(n^1, INF)

(28) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)
app(gen_nil:cons:f6_0(n2353_0), gen_nil:cons:f6_0(b)) → gen_nil:cons:f6_0(+(n2353_0, b)), rt ∈ Ω(1 + n2353₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(29) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(30) BOUNDS(n^1, INF)

(31) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)
length(gen_nil:cons:f6_0(n1957_0)) → gen_0':s7_0(n1957_0), rt ∈ Ω(1 + n1957₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(32) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(33) BOUNDS(n^1, INF)

(34) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)
leq(gen_0':s7_0(n1508_0), gen_0':s7_0(n1508_0)) → true, rt ∈ Ω(1 + n1508₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(35) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(36) BOUNDS(n^1, INF)

(37) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)
sndsplit(gen_0':s7_0(n717_0), gen_nil:cons:f6_0(n717_0)) → gen_nil:cons:f6_0(0), rt ∈ Ω(1 + n717₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(38) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(39) BOUNDS(n^1, INF)

(40) Obligation:

Innermost TRS:
Rules:
fstsplit(0', x) → nil
fstsplit(s(n), nil) → nil
fstsplit(s(n), cons(h, t)) → cons(h, fstsplit(n, t))
sndsplit(0', x) → x
sndsplit(s(n), nil) → nil
sndsplit(s(n), cons(h, t)) → sndsplit(n, t)
empty(nil) → true
empty(cons(h, t)) → false
leq(0', m) → true
leq(s(n), 0') → false
leq(s(n), s(m)) → leq(n, m)
length(nil) → 0'
length(cons(h, t)) → s(length(t))
app(nil, x) → x
app(cons(h, t), x) → cons(h, app(t, x))
map_f(pid, nil) → nil
map_f(pid, cons(h, t)) → app(f(pid, h), map_f(pid, t))
head(cons(h, t)) → h
tail(cons(h, t)) → t
ring(st_1, in_2, st_2, in_3, st_3, m) → if_1(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_1)))
if_1(st_1, in_2, st_2, in_3, st_3, m, false) → ring(sndsplit(m, st_1), cons(fstsplit(m, st_1), in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_2(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_2)))
if_2(st_1, in_2, st_2, in_3, st_3, m, true) → if_3(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_2)))
if_3(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, sndsplit(m, st_2), cons(fstsplit(m, st_2), in_3), st_3, m)
if_2(st_1, in_2, st_2, in_3, st_3, m, false) → if_4(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(two, head(in_2)), st_2))))
if_4(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, tail(in_2), sndsplit(m, app(map_f(two, head(in_2)), st_2)), cons(fstsplit(m, app(map_f(two, head(in_2)), st_2)), in_3), st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_5(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(two, head(in_2))))
if_5(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, tail(in_2), st_2, in_3, st_3, m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_6(st_1, in_2, st_2, in_3, st_3, m, leq(m, length(st_3)))
if_6(st_1, in_2, st_2, in_3, st_3, m, true) → if_7(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, st_3)))
if_7(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, in_3, sndsplit(m, st_3), m)
if_6(st_1, in_2, st_2, in_3, st_3, m, false) → if_8(st_1, in_2, st_2, in_3, st_3, m, empty(fstsplit(m, app(map_f(three, head(in_3)), st_3))))
if_8(st_1, in_2, st_2, in_3, st_3, m, false) → ring(st_1, in_2, st_2, tail(in_3), sndsplit(m, app(map_f(three, head(in_3)), st_3)), m)
ring(st_1, in_2, st_2, in_3, st_3, m) → if_9(st_1, in_2, st_2, in_3, st_3, m, empty(map_f(three, head(in_3))))
if_9(st_1, in_2, st_2, in_3, st_3, m, true) → ring(st_1, in_2, st_2, tail(in_3), st_3, m)

Types:
fstsplit :: 0':s → nil:cons:f → nil:cons:f
0' :: 0':s
nil :: nil:cons:f
s :: 0':s → 0':s
cons :: nil:cons:f → nil:cons:f → nil:cons:f
sndsplit :: 0':s → nil:cons:f → nil:cons:f
empty :: nil:cons:f → true:false
true :: true:false
false :: true:false
leq :: 0':s → 0':s → true:false
length :: nil:cons:f → 0':s
app :: nil:cons:f → nil:cons:f → nil:cons:f
map_f :: two:three → nil:cons:f → nil:cons:f
f :: two:three → nil:cons:f → nil:cons:f
head :: nil:cons:f → nil:cons:f
tail :: nil:cons:f → nil:cons:f
ring :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_1 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_2 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_3 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_4 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
two :: two:three
if_5 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_6 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_7 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
if_8 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
three :: two:three
if_9 :: nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → nil:cons:f → 0':s → true:false → ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
hole_nil:cons:f1_0 :: nil:cons:f
hole_0':s2_0 :: 0':s
hole_true:false3_0 :: true:false
hole_two:three4_0 :: two:three
hole_ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_95_0 :: ring:if_1:if_2:if_3:if_4:if_5:if_6:if_7:if_8:if_9
gen_nil:cons:f6_0 :: Nat → nil:cons:f
gen_0':s7_0 :: Nat → 0':s

Lemmas:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

Generator Equations:
gen_nil:cons:f6_0(0) ⇔ nil
gen_nil:cons:f6_0(+(x, 1)) ⇔ cons(nil, gen_nil:cons:f6_0(x))
gen_0':s7_0(0) ⇔ 0'
gen_0':s7_0(+(x, 1)) ⇔ s(gen_0':s7_0(x))

No more defined symbols left to analyse.

(41) LowerBoundsProof (EQUIVALENT transformation)

The lowerbound Ω(n¹) was proven with the following lemma:
fstsplit(gen_0':s7_0(n9_0), gen_nil:cons:f6_0(n9_0)) → gen_nil:cons:f6_0(n9_0), rt ∈ Ω(1 + n9₀)

(42) BOUNDS(n^1, INF)